choicef(${\it xm}$; $T$; $x$.$P$($x$)) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$case ${\it xm}$(\{$y$:$T$$\mid$ $P$($y$)\} ) of inl($z$) =$>$ $z$ $\mid$ inr($w$) =$>$ "???"